mba_boy - cr3 2024
ゲームボーイ製のフラグチェッカー
https://scrapbox.io/files/6694d7a35ff235001c8491a0.png
最初はコードの領域がディスアセンブルされていなかったりするので、バイナリを読んでそれっぽいところを手動でディスアセンブルする(重要)
2レジスタのconcatもうまく扱えていないので、うまくコードの意図をつかむ力が必要そう
メモリを眺めるとc0d2に入力したフラグが保存されていることがわかる
そこへアクセスしているコードを確認する
すると怪しそうな関数FUN_062bがみつかる
code: fun_042d.c
void FUN_042d(void)
{
bool bVar1;
byte bVar2;
int iVar3;
int iVar4;
undefined uStack_6;
undefined uStack_5;
undefined uStack_4;
undefined2 uStack_3;
byte local_1;
DAT_c0e6 = 1;
DAT_c0e7 = 1;
bVar2 = FUN_062b(CONCAT11(DAT_c0e3,DAT_c0e2) + 1,&input);
uStack_6 = 4;
uStack_5 = 0xc0;
uStack_4 = 4;
local_1 = 0;
for (iVar4 = 0; bVar2 = (byte)((uint)iVar4 >> 8), bVar1 = (byte)iVar4 < 0x12, bVar2 < bVar1;
iVar4 = iVar4 + 1) {
FUN_2311(bVar2 - bVar1,(uint)local_1 << 8);
for (iVar3 = 0; (byte)((uint)iVar3 >> 8) < ((byte)iVar3 < 5); iVar3 = iVar3 + 1) {
print_string?(uStack_3);
}
local_1 = local_1 + 1;
}
return;
}
code:fun_062b.c
undefined FUN_062b(undefined2 param_1,byte *param_2)
{
byte bVar1;
byte bVar2;
byte bVar3;
byte bVar4;
byte bVar5;
byte bVar6;
byte bVar7;
byte bVar8;
byte bVar9;
byte bVar10;
byte bVar11;
byte bVar12;
byte bVar13;
byte bVar14;
byte bVar15;
byte bVar16;
byte bVar17;
byte bVar18;
byte bVar19;
byte bVar20;
byte bVar21;
byte bVar22;
byte bVar23;
byte bVar24;
byte bVar25;
byte bVar26;
byte bVar27;
byte bVar28;
byte bVar29;
byte bVar30;
byte bVar31;
byte bVar32;
undefined uVar33;
byte bVar34;
byte bVar35;
bVar35 = (byte)((uint)param_1 >> 8);
bVar34 = (byte)param_1;
bVar1 = *param_2;
bVar17 = ~(~bVar1 & bVar9);
bVar18 = ~(~bVar2 & bVar10);
bVar19 = ~(~bVar3 & bVar11);
bVar20 = ~(~bVar4 & bVar12);
bVar21 = ~(~bVar5 & bVar13);
bVar22 = ~(~bVar6 & bVar14);
bVar23 = ~(~bVar7 & bVar15);
bVar24 = ~(~bVar8 & bVar16);
bVar17 = ~(~(bVar17 & bVar9) & ~(~bVar1 & bVar17));
bVar18 = ~(~(bVar18 & bVar10) & ~(~bVar2 & bVar18));
bVar19 = ~(~(bVar19 & bVar11) & ~(~bVar3 & bVar19));
bVar20 = ~(~(bVar20 & bVar12) & ~(~bVar4 & bVar20));
bVar21 = ~(~(bVar21 & bVar13) & ~(~bVar5 & bVar21));
bVar22 = ~(~(bVar22 & bVar14) & ~(~bVar6 & bVar22));
bVar23 = ~(~(bVar23 & bVar15) & ~(~bVar7 & bVar23));
bVar24 = ~(~(bVar24 & bVar16) & ~(~bVar8 & bVar24));
bVar25 = ~(bVar17 & ~(bVar1 | ~bVar9));
bVar26 = ~(bVar18 & ~(bVar2 | ~bVar10));
bVar27 = ~(bVar19 & ~(bVar3 | ~bVar11));
bVar28 = ~(bVar20 & ~(bVar4 | ~bVar12));
bVar29 = ~(bVar21 & ~(bVar5 | ~bVar13));
bVar30 = ~(bVar22 & ~(bVar6 | ~bVar14));
bVar31 = ~(bVar23 & ~(bVar7 | ~bVar15));
bVar32 = ~(bVar24 & ~(bVar8 | ~bVar16));
bVar17 = ~(~bVar9 | bVar1) | ~(bVar17 & bVar25) & ~(bVar25 & ~(bVar1 | ~bVar9));
bVar18 = ~(~bVar10 | bVar2) | ~(bVar18 & bVar26) & ~(bVar26 & ~(bVar2 | ~bVar10));
bVar19 = ~(~bVar11 | bVar3) | ~(bVar19 & bVar27) & ~(bVar27 & ~(bVar3 | ~bVar11));
bVar20 = ~(~bVar12 | bVar4) | ~(bVar20 & bVar28) & ~(bVar28 & ~(bVar4 | ~bVar12));
bVar21 = ~(~bVar13 | bVar5) | ~(bVar21 & bVar29) & ~(bVar29 & ~(bVar5 | ~bVar13));
bVar22 = ~(~bVar14 | bVar6) | ~(bVar22 & bVar30) & ~(bVar30 & ~(bVar6 | ~bVar14));
bVar23 = ~(~bVar15 | bVar7) | ~(bVar23 & bVar31) & ~(bVar31 & ~(bVar7 | ~bVar15));
bVar24 = ~(~bVar16 | bVar8) | ~(bVar24 & bVar32) & ~(bVar32 & ~(bVar8 | ~bVar16));
bVar17 = ~(~(~(bVar17 & bVar34) & bVar34) & ~(~(bVar17 & bVar34) & bVar17));
bVar18 = ~(~(~(bVar18 & bVar35) & bVar35) & ~(~(bVar18 & bVar35) & bVar18));
if ((((bVar17 == 0x7e) && (bVar18 == 0x60)) && (bVar19 == 0x77)) &&
(((bVar20 == 0x4c && (bVar21 == 0xd)) &&
((bVar22 == 0xc && ((bVar23 == 0x49 && (bVar24 == 0x4b)))))))) {
if ((((byte)(~(~(bVar17 & bVar1) & bVar1) & ~(~(bVar17 & bVar1) & bVar17)) == 0xc2) &&
(((((byte)(~(~(bVar18 & bVar2) & bVar2) & ~(~(bVar18 & bVar2) & bVar18)) == 0xcd &&
((byte)(~(~(bVar19 & bVar3) & bVar3) & ~(~(bVar19 & bVar3) & bVar19)) == 0xbb)) &&
((byte)(~(~(bVar20 & bVar4) & bVar4) & ~(~(bVar20 & bVar4) & bVar20)) == 200)) &&
(((byte)(~(~(bVar21 & bVar5) & bVar5) & ~(~(bVar21 & bVar5) & bVar21)) == 0xb1 &&
((byte)(~(~(bVar22 & bVar6) & bVar6) & ~(~(bVar22 & bVar6) & bVar22)) == 0xa6)))))) &&
((byte)(~(~(~(bVar23 & bVar7) & bVar7) & ~(~(bVar23 & bVar7) & bVar23)) + 0x83 |
~(~(~(bVar24 & bVar8) & bVar8) & ~(~(bVar24 & bVar8) & bVar24))) == 0)) {
if ((((byte)(~(~(bVar17 & bVar9) & bVar9) & ~(~(bVar17 & bVar9) & bVar17)) == 0xac) &&
((byte)(~(~(bVar18 & bVar10) & bVar10) & ~(~(bVar18 & bVar10) & bVar18)) == 0xad)) &&
((((byte)(~(~(bVar19 & bVar11) & bVar11) & ~(~(bVar19 & bVar11) & bVar19)) == 0xcc &&
((((byte)(~(~(bVar20 & bVar12) & bVar12) & ~(~(bVar20 & bVar12) & bVar20)) == 0x84 &&
((byte)(~(~(bVar21 & bVar13) & bVar13) & ~(~(bVar21 & bVar13) & bVar21)) == 0xbc)) &&
((byte)(~(~(bVar22 & bVar14) & bVar14) & ~(~(bVar22 & bVar14) & bVar22)) == 0xaa)))) &&
(((byte)(~(~(bVar23 & bVar15) & bVar15) & ~(~(bVar23 & bVar15) & bVar23)) == 0xcb &&
((byte)(~(~(bVar24 & bVar16) & bVar16) & ~(~(bVar24 & bVar16) & bVar24)) == 0xb4)))))) {
uVar33 = 3;
}
else {
uVar33 = 2;
}
}
else {
uVar33 = 1;
}
}
else {
uVar33 = 0;
}
return uVar33;
}
z3で解くとフラグが手に入る
code: solve.py
from z3 import *
param_1_high = BitVec('param_1_high', 8)
param_1_low = BitVec('param_1_low', 8)
bVar35 = param_1_high
bVar34 = param_1_low
bVar17 = ~(~bVar1 & bVar9);
bVar18 = ~(~bVar2 & bVar10);
bVar19 = ~(~bVar3 & bVar11);
bVar20 = ~(~bVar4 & bVar12);
bVar21 = ~(~bVar5 & bVar13);
bVar22 = ~(~bVar6 & bVar14);
bVar23 = ~(~bVar7 & bVar15);
bVar24 = ~(~bVar8 & bVar16);
bVar17 = ~(~(bVar17 & bVar9) & ~(~bVar1 & bVar17));
bVar18 = ~(~(bVar18 & bVar10) & ~(~bVar2 & bVar18));
bVar19 = ~(~(bVar19 & bVar11) & ~(~bVar3 & bVar19));
bVar20 = ~(~(bVar20 & bVar12) & ~(~bVar4 & bVar20));
bVar21 = ~(~(bVar21 & bVar13) & ~(~bVar5 & bVar21));
bVar22 = ~(~(bVar22 & bVar14) & ~(~bVar6 & bVar22));
bVar23 = ~(~(bVar23 & bVar15) & ~(~bVar7 & bVar23));
bVar24 = ~(~(bVar24 & bVar16) & ~(~bVar8 & bVar24));
bVar25 = ~(bVar17 & ~(bVar1 | ~bVar9));
bVar26 = ~(bVar18 & ~(bVar2 | ~bVar10));
bVar27 = ~(bVar19 & ~(bVar3 | ~bVar11));
bVar28 = ~(bVar20 & ~(bVar4 | ~bVar12));
bVar29 = ~(bVar21 & ~(bVar5 | ~bVar13));
bVar30 = ~(bVar22 & ~(bVar6 | ~bVar14));
bVar31 = ~(bVar23 & ~(bVar7 | ~bVar15));
bVar32 = ~(bVar24 & ~(bVar8 | ~bVar16));
bVar17 = ~(~bVar9 | bVar1) | ~(bVar17 & bVar25) & ~(bVar25 & ~(bVar1 | ~bVar9));
bVar18 = ~(~bVar10 | bVar2) | ~(bVar18 & bVar26) & ~(bVar26 & ~(bVar2 | ~bVar10));
bVar19 = ~(~bVar11 | bVar3) | ~(bVar19 & bVar27) & ~(bVar27 & ~(bVar3 | ~bVar11));
bVar20 = ~(~bVar12 | bVar4) | ~(bVar20 & bVar28) & ~(bVar28 & ~(bVar4 | ~bVar12));
bVar21 = ~(~bVar13 | bVar5) | ~(bVar21 & bVar29) & ~(bVar29 & ~(bVar5 | ~bVar13));
bVar22 = ~(~bVar14 | bVar6) | ~(bVar22 & bVar30) & ~(bVar30 & ~(bVar6 | ~bVar14));
bVar23 = ~(~bVar15 | bVar7) | ~(bVar23 & bVar31) & ~(bVar31 & ~(bVar7 | ~bVar15));
bVar24 = ~(~bVar16 | bVar8) | ~(bVar24 & bVar32) & ~(bVar32 & ~(bVar8 | ~bVar16));
bVar17 = ~(~(~(bVar17 & bVar34) & bVar34) & ~(~(bVar17 & bVar34) & bVar17));
bVar18 = ~(~(~(bVar18 & bVar35) & bVar35) & ~(~(bVar18 & bVar35) & bVar18));
s = Solver()
s.add(bVar17 == 0x7e)
s.add(bVar18 == 0x60)
s.add(bVar19 == 0x77)
s.add(bVar20 == 0x4c)
s.add(bVar21 == 0xd)
s.add(bVar22 == 0xc)
s.add(bVar23 == 0x49)
s.add(bVar24 == 0x4b)
s.add((~(~(bVar17 & bVar1) & bVar1) & ~(~(bVar17 & bVar1) & bVar17)) == 0xc2)
s.add((~(~(bVar18 & bVar2) & bVar2) & ~(~(bVar18 & bVar2) & bVar18)) == 0xcd)
s.add((~(~(bVar19 & bVar3) & bVar3) & ~(~(bVar19 & bVar3) & bVar19)) == 0xbb)
s.add((~(~(bVar20 & bVar4) & bVar4) & ~(~(bVar20 & bVar4) & bVar20)) == 200)
s.add((~(~(bVar21 & bVar5) & bVar5) & ~(~(bVar21 & bVar5) & bVar21)) == 0xb1)
s.add((~(~(bVar22 & bVar6) & bVar6) & ~(~(bVar22 & bVar6) & bVar22)) == 0xa6)
s.add((~(~(~(bVar23 & bVar7) & bVar7) & ~(~(bVar23 & bVar7) & bVar23)) + 0x83 | ~(~(~(bVar24 & bVar8) & bVar8) & ~(~(bVar24 & bVar8) & bVar24))) == 0)
s.add((~(~(bVar17 & bVar9) & bVar9) & ~(~(bVar17 & bVar9) & bVar17)) == 0xac)
s.add((~(~(bVar18 & bVar10) & bVar10) & ~(~(bVar18 & bVar10) & bVar18)) == 0xad)
s.add((~(~(bVar19 & bVar11) & bVar11) & ~(~(bVar19 & bVar11) & bVar19)) == 0xcc)
s.add((~(~(bVar20 & bVar12) & bVar12) & ~(~(bVar20 & bVar12) & bVar20)) == 0x84)
s.add((~(~(bVar21 & bVar13) & bVar13) & ~(~(bVar21 & bVar13) & bVar21)) == 0xbc)
s.add((~(~(bVar22 & bVar14) & bVar14) & ~(~(bVar22 & bVar14) & bVar22)) == 0xaa)
s.add((~(~(bVar23 & bVar15) & bVar15) & ~(~(bVar23 & bVar15) & bVar23)) == 0xcb)
s.add((~(~(bVar24 & bVar16) & bVar16) & ~(~(bVar24 & bVar16) & bVar24)) == 0xb4)
s.check()
m = s.model()
''.join([chr(mit.as_long())for it in param_2])